(* $Id: verificationGenerationEnv.ml 117 2007-10-21 17:27:07Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open XCoreSyntax
open XCoreSyntaxExt
open XCoreInternals

open Options
open Arg

type options = {
  mutable trace_proofs : bool;
  mutable trace_proofs_more : bool;
  mutable trace_proofs_auto_failed : bool;
}

let options = { 
  trace_proofs = false;
  trace_proofs_more = false;
  trace_proofs_auto_failed = false;
} 

type t =
    {
      (* Values. *)
      ids       : (Var.Atom.t * (Position.t * type_scheme)) list;

      (* Logic objects : predicates, logic functions and logic values. *)
      logic_ids      : (Var.Atom.t * (Position.t * formula_type_scheme)) list;
      predicate_defs : (Var.Atom.t * predicate_definition) list;
      logicfun_defs  : (Var.Atom.t * logic_function_definition) list;

      (* Hypothesis. *)
      facts     : (UniqueIdentifier.t * lformula) list;

      (* Type variables and type constructors. *)
      tvars     : (Var.Atom.t * kind) list;
      type_defs : (Var.Atom.t * type_definition) list;
      datacons  : (Var.Atom.t * Var.Atom.t) list;

      (* Trace source identifier to pretty-print correctly. *)
      idmap     : var XCoreSyntax.Identifier.Map.t;
      atomidmap : Var.AtomIdMap.t;

      (* The internal representation of types uses an environment. *)
      ienv      : XCoreInternals.env;

      (* The first order encoding of this environment. *)
      pfol	: PFOLEncodedEnv.env
    }

type proofs = (t * lformula) list

let bind_atom x env =
  let aim = Var.AtomIdMap.add x env.atomidmap in
  let id = Var.AtomIdMap.find x aim in
    { env with
	idmap = XCoreSyntax.Identifier.Map.add id x env.idmap;
	atomidmap = aim
    }

let idmap env = 
  env.idmap

let atomidmap env = 
  env.atomidmap 

let ienv env = 
  env.ienv

let initial_env = 
  {
    ids = [];
    logic_ids = [];
    idmap = XCoreSyntax.Identifier.Map.empty;
    atomidmap = Var.AtomIdMap.empty;
    ienv = XCoreInternals.empty_env;
    tvars = [];
    predicate_defs = [];
    logicfun_defs = [];
    type_defs = [];
    facts = [];
    datacons = [];
    pfol = PFOLEncodedEnv.empty
  }

let rec unsafe_export_formula ids f = 
  try 
    export_formula ids f
  with Var.Atom.Unknown a ->
    Printf.eprintf "WARNING INTERNAL ERROR: unbound %s\n" 
      (PIdentifier.as_string (Var.Atom.basename a));
    unsafe_export_formula (Var.AtomIdMap.add a ids) f

let print_formula env f = 
  let xf = unsafe_export_formula (atomidmap env) f in
    XCorePrinter.formula_as_string xf

let bind_type_scheme pos env x s = 
  bind_atom x
    { env with 
	ids = (x, (pos, s)) :: env.ids;
	pfol = fst (PFOLEncodedEnv.bind_value pos env.pfol x s)
    }

let bind_dataconstructor_type_scheme pos env x s = 
  bind_atom x
    { env with 
	ids = (x, (pos, s)) :: env.ids;
    }

let bind pos env x ty = 
  bind_type_scheme pos env x (monoscheme ty)

let lookup pos env x =
  try
    snd (snd (List.find (fun (y, _) -> Var.Atom.equal x y) env.ids))
  with Not_found ->
    assert false

let bind_logic_scheme pos env p s = 
  bind_atom p { env with logic_ids = (p, (pos, s)) :: env.logic_ids; }

let bind_logic pos env p ty =
  bind_logic_scheme pos env p (formula_monoscheme ty)

let rec lift_term_type = function
  | TPrimitive p -> 
      FTPrimitive p 

  | TVar x ->
      FTVar x

  | TArrow (ins, outs) ->
      FTCArrow (lift_term_type ins, lift_term_type outs)

  | TProd ts ->
      FTProd (List.map lift_term_type ts)

  | TApp (tycon, ts) ->
      FTApp (tycon, List.map lift_term_type ts)

let lift_type_scheme (TScheme abs) =
  let (vs, ty) = open_scheme_abs abs in
    FTScheme (create_formula_scheme_abs (vs, lift_term_type ty))

let lookup_logic pos env x = 
  try 
    snd (snd (List.find (fun (y, _) -> Var.Atom.equal x y) env.logic_ids))
  with Not_found ->
    lift_type_scheme (lookup pos env x)

let introduce_rigid_type_variable pos env v = 
  bind_atom v 
    {
      env with 
	tvars = (v, KStar) :: env.tvars;
	ienv = XCoreInternals.introduce_rigid_type_variables env.ienv [v];
	pfol = PFOLEncodedEnv.introduce_rigid_type_variables pos env.pfol [(v, KStar)]
    }

let introduce_rigid_type_variables pos vs env =
  List.fold_left (introduce_rigid_type_variable pos) env vs

let bind_type_constructor pos env t k =
  bind_atom t 
    { env with
	tvars = (t, k) :: env.tvars;
	ienv = XCoreInternals.introduce_rigid_type_variables env.ienv [t] 
    }

let bind_type_definition pos env t k def = 
  { (bind_type_constructor pos env t k)
    with 
      type_defs = (t, def) :: env.type_defs;
      pfol = PFOLEncodedEnv.bind_type_definition pos env.pfol t k def;
      datacons = match def with
	| DAlgebraic (_, ds) ->
	    List.fold_left (fun datacons (k, _, _) -> (k, t) :: datacons) 
	      env.datacons ds
	| _ -> env.datacons
  }

let bind_predicate pos env p s = 
  { (bind_logic_scheme pos env p s)
    with pfol = PFOLEncodedEnv.bind_predicate_type_scheme pos env.pfol p s } 

let display_def env pos p s = function
  | PDInductive cases ->
      Printf.eprintf "INV: %s\n"
	(print_formula env 
	   (inductive_inversion pos p s cases).fvalue)
  | _ -> ()

let bind_predicate_definition pos env p s def =
  let env = bind_logic_scheme pos env p s in
    { env
      with 
	predicate_defs = (p, def) :: env.predicate_defs;
	pfol = PFOLEncodedEnv.bind_predicate_definition pos env.pfol p s def 
    }  

let bind_logic_value pos env p ty =
  let s = formula_monoscheme ty in
    { (bind_logic pos env p ty)
      with 
	pfol = fst (PFOLEncodedEnv.bind_logic_value pos env.pfol p s)
    }  

let bind_logic_function pos env p s = 
  { (bind_logic_scheme pos env p s) 
    with 
      pfol = PFOLEncodedEnv.bind_logic_function pos env.pfol p s 
  }

let bind_logic_function_definition pos env p s def = 
  { (bind_logic_function pos env p s) 
    with 
      pfol = PFOLEncodedEnv.bind_logic_function_definition pos env.pfol p s def;
      logicfun_defs = (p, def) :: env.logicfun_defs
  }


let handle_error env f =
  try
    f ()
  with PFOLEncoding.ErrorWhenEncode f -> 
    Printf.printf "%s\nENCODING ERROR:\n%s\n\n" 
      (Position.string_of_pos f.fpos)
      (print_formula env f.fvalue);
    exit 1

let hypothesis_id pos = function
  | None -> UniqueIdentifier.fresh (pos, "hypothesis")
  | Some n -> n

let assume pos env ?name f = 
  let f = XCoreNormalizeFormula.lnormalize f in
    if options.trace_proofs_more then 
      Printf.printf "Assume %s\n" (print_formula env f.fvalue);  
    handle_error env 
      (fun () -> { env with  
		     facts = (hypothesis_id pos name, f) :: env.facts;
		     pfol = PFOLEncodedEnv.bind_fact pos env.pfol f
		 })


let show_one pos auto (env, proofs) ?name f = 
  let f = XCoreNormalizeFormula.lnormalize f in
    if options.trace_proofs_more then 
      Printf.printf "%s\nSHOW ?:\n%s\n\n" 
	(Position.string_of_pos pos)
	(print_formula env (XCoreNormalizeFormula.normalize f.fvalue)); 
    
    let (_, ef) = PFOLEncoding.encode_formula_as_predicate f.fpos env.pfol f in
    let (auto_ret, auto_filenames) = AutomaticProver.prove f (env.pfol, ef) in
    let auto_filenames = String.concat ", " auto_filenames in
    if not auto_ret then
      if auto then 
	Error.error "automatic prover" pos 
	  (Printf.sprintf "failed to prove:\n%s\n%s\n%!" 
	     (print_formula env f.fvalue) auto_filenames)
      else  (
	if options.trace_proofs || options.trace_proofs_auto_failed then 
	  Printf.printf "%s\nfailed to automatically prove:\n%s\n%s\n%!" 
	    (Position.string_of_pos pos)
	    (print_formula env f.fvalue) auto_filenames;
	(env, f) :: proofs
      ) else (
      if options.trace_proofs then 
	Printf.printf "%s\nsucceed to prove:\n%s\n%s\n%!" 
	  (Position.string_of_pos pos)
	  (print_formula env f.fvalue) auto_filenames; 
      proofs)

let show pos auto (env, proofs) ?name f = 
  List.fold_left (fun proofs -> show_one pos auto (env, proofs) ~name) 
    proofs (destruct_conjs f)
    
let have auto pos (env, proofs) ?name f = 
  handle_error env 
    (fun () -> (assume pos env ?name f, 
		show pos auto (env, proofs) ~name f))

let assume_eq pos env ty t1 t2 = 
  assume pos env (mk_lformula pos (mk_feq pos ty t1 t2))

let have_eq_pattern pos env ty t p =
  assume pos env 
    (mk_lformula pos (mk_feq pos ty 
			(mk_fannot pos t ty)
			(mk_fannot pos (pattern_as_logic_value pos p) ty)))

let have_neq_pattern pos env ty t ex_ts fragment p =
  let f = 
    mk_fforalltys pos ex_ts
      (mk_lforall pos 
	 (XCoreLifting.to_logic_bindings fragment)
	 (mk_fneq pos ty 
	    (mk_fannot pos t ty) 
	    (mk_fannot pos (pattern_as_logic_value pos p) ty)))
  in
    assume pos env (mk_lformula pos f)

let empty_proofs = 
  []

let is_dataconstructor k env = 
  List.mem_assoc k env.datacons

let pcons next c = 
  PConsComponent (create_pcons_abs (c, next))

let type_def_of x env = 
  try
    List.assoc x env.type_defs
  with Not_found -> DeferredType

let proof_as_term (env, f) = 
  let f = CFact (Lemma (UniqueIdentifier.fresh (f.fpos, "goal")), f) in
  let facts = 
    List.map (fun (n, f) -> CFact (Axiom n, f)) env.facts 
  in
  let types = 
    List.map (fun (x, k) -> CTypeDef (x, k, type_def_of x env)) env.tvars 
  in
  let logic_ids =
    List.map 
      (fun (f, (pos, s)) -> 
	 try 
	   let fdef = List.assoc f env.logicfun_defs in
	     CLogicFunction (f, s, fdef)
	 with Not_found -> 
	   try 
	     let pdef = List.assoc f env.predicate_defs in
	       CPredicate (f, s, pdef)
	   with Not_found ->
	     CPredicate (f, s, PDAbbrev (mk_lformula pos  FDeferred)))
      env.logic_ids
  in
  let ids = 
    List.map (fun (x, (pos, t)) -> 
		CPredicate (x, XCoreLifting.lift_type_scheme t, 
			    PDAbbrev (mk_lformula pos FDeferred)))
      (List.filter (fun (x, _) -> not (is_dataconstructor x env)) env.ids)
  in
    List.fold_left pcons PEmpty (f :: facts @ logic_ids @ ids @ types)

let export_proof (env, f) = 
  let t = proof_as_term (env, f) in
    try 
      export_program Var.AtomIdMap.empty t
  with Var.Atom.Unknown a ->
    Printf.eprintf "WARNING INTERNAL ERROR: unbound %s\n" 
      (PIdentifier.as_string (Var.Atom.basename a));
    exit 1

let options () = 
  mk_local_options 
    {
      env         = options;
      postprocess = (fun x -> x);
      options     = Arg.align [
	"--trace", 
	Unit (fun x -> options.trace_proofs <- true), 
	" Show the result of type inference."
      ]
    } 
